Nuprl Definition : loc-ordered
0,22
postcript
pdf
loc-ordered(
es
;
L
) == l-ordered(E;
x
,
y
.(
x
<loc
y
);
L
)
latex
clarification:
loc-ordered(
es
;
L
) == l-ordered(es-E(
es
);
x
,
y
.es-locl(
es
;
x
;
y
);
L
)
latex
Definitions
l-ordered(
T
;
x
,
y
.
R
(
x
;
y
);
L
)
,
E
,
(
e
<loc
e'
)
FDL editor aliases
loc-ordered
origin